es:ES, e, a:E.
a loc e 
 ((first(a)))
 (es-le-before(es;e) = (es-le-before(es;pred(a)) @ [a, e])  (E List)) 

latex

Definitions

t  T, s = t, x:AB(x), x:A. B(x), e loc e' , ES, E, P  Q, True, {x:A| B(x)} , [e, e'], A, before(e), as @ bs, es-le-before(es;e), type List, x:A  B(x), a:A fp B(a), <a, b>, strong-subtype(A;B), pred(e), T, Type, , , ||as||, Void, x:A.B(x), Top, S  T, , {T}, s ~ t, SQType(T), let x,y = A in B(x;y), t.1, [car / cdr], P & Q, P  Q, P  Q, A  B, i  j , [], A List, first(e), b, b, ff, , False, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p  q, p  q, p q, tt, Unit, left + right

Lemmas

eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, es-le-before-partition, event system wf, not wf, assert wf, es-first wf, non neg length, cons one one, guard wf, nat wf, length wf nat, top wf, es-pred wf, member wf, append wf, squash wf, true wf, es-E wf, es-before wf, es-le-before wf, es-interval wf, es-le wf